1 /-
2 Copyright (c) 2018 Mario Carneiro. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Mario Carneiro
5
6 Archimedean groups and fields.
7 -/
8 import algebra.group_power algebra.field_power algebra.floor
src └─────────────────┘ └─────────────────┘ └───────────┘
9 import data.rat tactic.linarith
src └──────┘ └─────────────┘
10
11 variables {α : Type*}
id ┴
typ ┴
12
13 open_locale add_monoid
14
15 class archimedean (α) [ordered_comm_monoid α] : Prop :=
id ┴ └─────────────────┘ ┴
src └─────────────────┘
typ ┴ └─────────────────┘ ┴
doc └─────────────────┘
16 (arch : ∀ (x : α) {y}, 0 < y → ∃ n : ℕ, x ≤ n • y)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
17
18 theorem exists_nat_gt [linear_ordered_semiring α] [archimedean α]
id └─────────────────────┘ ┴ └─────────┘ ┴
src └─────────────────────┘ └─────────┘
typ └─────────────────────┘ ┴ └─────────┘ ┴
19 (x : α) : ∃ n : ℕ, x < n :=
id ┴ ┴ ┴┴ ┴ ┴ ┴
src ┴ ┴┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴
20 let ⟨n, h⟩ := archimedean.arch x zero_lt_one in
id └─┘ ┴ └──────────────┘ ┴ └─────────┘
src └──────────────┘ └─────────┘
typ └─┘ ┴ └──────────────┘ ┴ └─────────┘
21 ⟨n+1, lt_of_le_of_lt (by rwa ← add_monoid.smul_one)
id ┴ └────────────┘ └─────────────────┘
src ┴ └────────────┘ └────┘└─────────────────┘
typ ┴ └────────────┘ └────┘└─────────────────┘
doc └────┘
txt └────┘
par └────┘
pid └─┘
st └────────────────────────┘
22 (nat.cast_lt.2 (nat.lt_succ_self _))⟩
id └─────────┘┴ └──────────────┘
src └─────────┘┴ └──────────────┘
typ └─────────┘┴ └──────────────┘
23
24 section linear_ordered_ring
25 variables [linear_ordered_ring α] [archimedean α]
id └─────────────────┘ └─────────┘
src └─────────────────┘ └─────────┘
typ └─────────────────┘ └─────────┘
26
27 lemma pow_unbounded_of_one_lt (x : α) {y : α}
id ┴ ┴
typ ┴ ┴
28 (hy1 : 1 < y) : ∃ n : ℕ, x < y ^ n :=
id ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
29 have hy0 : 0 < y - 1 := sub_pos_of_lt hy1,
id ┴ ┴ ┴ └───────────┘ └─┘
src ┴ ┴ └───────────┘
typ ┴ ┴ ┴ └───────────┘ └─┘
30 -- TODO `by linarith` fails to prove hy1'
31 have hy1' : (-1:α) ≤ y, from le_trans (neg_le_self zero_le_one) (le_of_lt hy1),
id ┴ ┴ ┴ ┴ └──────┘ └─────────┘ └─────────┘ └──────┘ └─┘
src ┴ ┴ └──────┘ └─────────┘ └─────────┘ └──────┘
typ ┴ ┴ ┴ ┴ └──────┘ └─────────┘ └─────────┘ └──────┘ └─┘
32 let ⟨n, h⟩ := archimedean.arch x hy0 in
id └─┘ ┴ ┴ └──────────────┘ ┴ └─┘
src └──────────────┘
typ └─┘ ┴ ┴ └──────────────┘ ┴ └─┘
33 ⟨n, calc x ≤ n • (y - 1) : h
id ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴
34 ... < 1 + n • (y - 1) : lt_one_add _
id ┴ ┴ ┴ ┴ └────────┘
src ┴ ┴ ┴ └────────┘
typ ┴ ┴ ┴ ┴ └────────┘
35 ... ≤ y ^ n : one_add_sub_mul_le_pow hy1' n⟩
id ┴ ┴ └────────────────────┘ └──┘
src ┴ └────────────────────┘
typ ┴ ┴ └────────────────────┘ └──┘
doc └────────────────────┘
36
37 /-- Every x greater than 1 is between two successive natural-number
38 powers of another y greater than one. -/
39 lemma exists_nat_pow_near {x : α} {y : α} (hx : 1 < x) (hy : 1 < y) :
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
40 ∃ n : ℕ, y ^ n ≤ x ∧ x < y ^ (n + 1) :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
41 have h : ∃ n : ℕ, x < y ^ n, from pow_unbounded_of_one_lt _ hy,
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └─────────────────────┘ └┘
src ┴ ┴┴ ┴ ┴ └─────────────────────┘
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └─────────────────────┘ └┘
42 by classical; exact let n := nat.find h in
id └──────┘
src └───────┘ └────┘ └────┘└──────┘┴ └───
typ └───────┘ └────┘ └────┘└──────┘┴ └───
doc └───────┘ └────┘ └────┘ ┴ └───
txt └───────┘ └────┘ └────┘ ┴ └───
par └───────┘ └────┘ └────┘ ┴ └───
pid ┴ └────┘ ┴ └───
st └────────────────────────────────────────
43 have hn : x < y ^ n, from nat.find_spec h,
id ┴ ┴ ┴ ┴ └───────────┘ ┴
src ─┘ └─────┘ ┴┴┴ ┴┴┴ └─────┘└───────────┘┴ └─
typ ─┘ └─────┘┴┴┴┴┴┴┴┴ └─────┘└───────────┘┴┴└─
doc ─┘ └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ └─
txt ─┘ └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ └─
par ─┘ └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ └─
pid ─┘ └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ └─
st ──────────────────────────────────────────────
44 have hnp : 0 < n, from nat.pos_iff_ne_zero.2 (λ hn0,
id └─────────────────┘
src ─┘ └───────┘ ┴ └─────────┘└─────────────────┘└─┘ └─────
typ ─┘ └───────┘ ┴ └─────────┘└─────────────────┘└─┘ └─────
doc ─┘ └───────┘ ┴ └─────────┘ └─┘ └─────
txt ─┘ └───────┘ ┴ └─────────┘ └─┘ └─────
par ─┘ └───────┘ ┴ └─────────┘ └─┘ └─────
pid ─┘ └───────┘ ┴ └─────────┘ └─┘ └─────
st ───────────────────────────────────────────────────────────
45 by rw [hn0, pow_zero] at hn; exact (not_lt_of_gt hn hx)),
id └─┘ └──────┘ └──────────┘ └┘ └┘
src ───┘ ┴└──┘ └┘└──────┘└─────┘└──────┘ └──────────┘┴ ┴ └───
typ ───┘ ┴└──┘└─┘└┘└──────┘└─────┘└──────┘ └──────────┘┴└┘┴└┘└───
doc ───┘ ┴└──┘ └┘ └─────┘└──────┘ ┴ ┴ └───
txt ───┘ ┴└──┘ └┘ └─────┘└──────┘ ┴ ┴ └───
par ───┘ ┴└──┘ └┘ └─────┘└──────┘ ┴ ┴ └───
pid ───┘ └───┘ └┘ └─────────────┘ ┴ ┴ └───
st ─────┘└──────┘└────────┘┴└────────────────────────────────┘└──
46 have hnsp : nat.pred n + 1 = n, from nat.succ_pred_eq_of_pos hnp,
id ┴ ┴ └─────────────────────┘
src ─┘ └──────┘ ┴ ┴┴└─┘┴┴ └─────────┘└─────────────────────┘┴ └─
typ ─┘ └──────┘ ┴ ┴┴└─┘┴┴ └─────────┘└─────────────────────┘┴ └─
doc ─┘ └──────┘ ┴ ┴ └─┘ ┴ └─────────┘ ┴ └─
txt ─┘ └──────┘ ┴ ┴ └─┘ ┴ └─────────┘ ┴ └─
par ─┘ └──────┘ ┴ ┴ └─┘ ┴ └─────────┘ ┴ └─
pid ─┘ └──────┘ ┴ ┴ └─┘ ┴ └─────────┘ ┴ └─
st ────────────────────────────────────────────────────────────────────────
47 have hltn : nat.pred n < n, from nat.pred_lt (ne_of_gt hnp),
id └─────────┘ └──────┘
src ─┘ └──────┘ ┴ ┴ ┴ └─────────────┘└─────────┘┴ └──────┘┴ └──
typ ─┘ └──────┘ ┴ ┴ ┴ └─────────────┘└─────────┘┴ └──────┘┴ └──
doc ─┘ └──────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ └──
txt ─┘ └──────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ └──
par ─┘ └──────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ └──
pid ─┘ └──────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ └──
st ───────────────────────────────────────────────────────────────────────
48 ⟨nat.pred n, le_of_not_lt (nat.find_min h hltn), by rwa hnsp⟩
id └──────┘ └──────────┘ └──────────┘ └──┘
src ─┘ └──────┘┴ └┘└──────────┘┴ └──────────┘┴ ┴ └─┘ ┴└──┘ └─
typ ─┘ └──────┘┴ └┘└──────────┘┴ └──────────┘┴ ┴ └─┘ ┴└──┘└──┘└─
doc ─┘ ┴ └┘ ┴ ┴ ┴ └─┘ ┴└──┘ └─
txt ─┘ ┴ └┘ ┴ ┴ ┴ └─┘ ┴└──┘ └─
par ─┘ ┴ └┘ ┴ ┴ ┴ └─┘ ┴└──┘ └─
pid ─┘ ┴ └┘ ┴ ┴ ┴ └─┘ └───┘ ┴└
st ────────────────────────────────────────────────────┘└───────┘└─
49
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
50 theorem exists_int_gt (x : α) : ∃ n : ℤ, x < n :=
id ┴ ┴ ┴┴ ┴ ┴ ┴
src ┴ ┴┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴
51 let ⟨n, h⟩ := exists_nat_gt x in ⟨n, by rwa ← coe_coe⟩
id └─┘ ┴ └───────────┘ ┴ └─────┘
src └───────────┘ └────┘└─────┘
typ └─┘ ┴ └───────────┘ ┴ └────┘└─────┘
doc └────┘└─────┘
txt └────┘
par └────┘
pid └─┘
st └────────────┘
52
53 theorem exists_int_lt (x : α) : ∃ n : ℤ, (n : α) < x :=
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
54 let ⟨n, h⟩ := exists_int_gt (-x) in ⟨-n, by rw int.cast_neg; exact neg_lt.1 h⟩
id └─┘ ┴ └───────────┘ ┴┴ ┴ └──────────┘ └────┘ ┴
src └───────────┘ ┴ ┴ └─┘└──────────┘ └────┘└────┘└─┘
typ └─┘ ┴ └───────────┘ ┴┴ ┴ └─┘└──────────┘ └────┘└────┘└─┘┴
doc └─┘ └────┘ └─┘
txt └─┘ └────┘ └─┘
par └─┘ └────┘ └─┘
pid ┴ ┴ └─┘
st └────────────────────────────────┘
55
56 theorem exists_floor (x : α) :
id ┴
typ ┴
57 ∃ (fl : ℤ), ∀ (z : ℤ), z ≤ fl ↔ (z : α) ≤ x :=
id ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
58 begin
st └─────
59 haveI := classical.prop_decidable,
id └──────────────────────┘
src └───────┘└──────────────────────┘
typ └───────┘└──────────────────────┘
doc └───────┘
txt └───────┘
par └───────┘
pid ┴└─┘
st ──────────────────────────────────┘└─
60 have : ∃ (ub : ℤ), (ub:α) ≤ x ∧ ∀ (z : ℤ), (z:α) ≤ x → z ≤ ub :=
id ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘┴└─────┘ ┴┴┴ ┴ └┘┴┴ ┴┴┴ └────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └───
typ └─────┘┴└─────┘ ┴┴┴ ┴ └┘┴┴ ┴┴┴ └────┘ ┴ ┴ ┴┴└┘ ┴┴┴ ┴ ┴ ┴ └───
doc └─────┘ └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └───
txt └─────┘ └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └───
par └─────┘ └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └───
pid └───┘└┘ └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └───
st ───────────────────────────────────────────────────────────────────
61 int.exists_greatest_of_bdd
id └────────────────────────┘
src ─┘└────────────────────────┘└
typ ─┘└────────────────────────┘└
doc ─┘ └
txt ─┘ └
par ─┘ └
pid ─┘ └
st ─────────────────────────────
62 (let ⟨n, hn⟩ := exists_int_gt x in ⟨n, λ z h',
id ┴ └┘ └───────────┘
src ───┘ ┴ └┘ └───┘└───────────┘┴ └──┘ └┘ └──────
typ ───┘ ┴ ┴└┘└┘└───┘└───────────┘┴ └──┘ └┘ └──────
doc ───┘ ┴ └┘ └───┘ ┴ └──┘ └┘ └──────
txt ───┘ ┴ └┘ └───┘ ┴ └──┘ └┘ └──────
par ───┘ ┴ └┘ └───┘ ┴ └──┘ └┘ └──────
pid ───┘ ┴ └┘ └───┘ ┴ └──┘ └┘ └──────
st ───────────────────────────────────────────────────
63 int.cast_le.1 $ le_trans h' $ le_of_lt hn⟩)
id └─────────┘ └──────┘
src ─────┘└─────────┘└─┘ ┴└──────┘┴ ┴ ┴ ┴ └──
typ ─────┘└─────────┘└─┘ ┴└──────┘┴ ┴ ┴ ┴ └──
doc ─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ └──
txt ─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ └──
par ─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ └──
pid ─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ └──
st ──────────────────────────────────────────────────
64 (let ⟨n, hn⟩ := exists_int_lt x in ⟨n, le_of_lt hn⟩),
id ┴ └┘ └───────────┘ ┴ └──────┘
src ───┘ ┴ └┘ └───┘└───────────┘┴ └──┘ └┘└──────┘┴ └┘
typ ───┘ ┴ ┴└┘└┘└───┘└───────────┘┴┴└──┘ └┘└──────┘┴ └┘
doc ───┘ ┴ └┘ └───┘ ┴ └──┘ └┘ ┴ └┘
txt ───┘ ┴ └┘ └───┘ ┴ └──┘ └┘ ┴ └┘
par ───┘ ┴ └┘ └───┘ ┴ └──┘ └┘ ┴ └┘
pid ───┘ ┴ └┘ └───┘ ┴ └──┘ └┘ ┴ └┘
st ───────────────────────────────────────────────────────┘└─
65 refine this.imp (λ fl h z, _),
id └──────┘
src └─────┘└──────┘┴ └─────────┘
typ └─────┘└──────┘┴ └─────────┘
doc └─────┘ ┴ └─────────┘
txt └─────┘ ┴ └─────────┘
par └─────┘ ┴ └─────────┘
pid ┴ ┴ └─────────┘
st ──────────────────────────────┘└─
66 cases h with h₁ h₂,
id ┴
src └────┘ └─────────┘
typ └────┘┴└─────────┘
doc └────┘ └─────────┘
txt └────┘ └─────────┘
par └────┘ └─────────┘
pid ┴ └─────────┘
st ───────────────────┘└─
67 exact ⟨λ h, le_trans (int.cast_le.2 h) h₁, h₂ z⟩,
id └──────┘ └─────────┘ └┘ └┘ ┴
src └────┘ └──┘└──────┘┴ └─────────┘└─┘ └┘ └┘ ┴ ┴
typ └────┘ └──┘└──────┘┴ └─────────┘└─┘ └┘└┘└┘└┘┴┴┴
doc └────┘ └──┘ ┴ └─┘ └┘ └┘ ┴ ┴
txt └────┘ └──┘ ┴ └─┘ └┘ └┘ ┴ ┴
par └────┘ └──┘ ┴ └─┘ └┘ └┘ ┴ ┴
pid ┴ └──┘ ┴ └─┘ └┘ └┘ ┴ ┴
st ─────────────────────────────────────────────────┘└─
68 end
st ──┘
69
70 end linear_ordered_ring
71
72 section linear_ordered_field
73
74 /-- Every positive x is between two successive integer powers of
75 another y greater than one. This is the same as `exists_int_pow_near'`,
76 but with ≤ and < the other way around. -/
77 lemma exists_int_pow_near [discrete_linear_ordered_field α] [archimedean α]
id └───────────────────────────┘ ┴ └─────────┘ ┴
src └───────────────────────────┘ └─────────┘
typ └───────────────────────────┘ ┴ └─────────┘ ┴
78 {x : α} {y : α} (hx : 0 < x) (hy : 1 < y) :
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
79 ∃ n : ℤ, y ^ n ≤ x ∧ x < y ^ (n + 1) :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
80 by classical; exact
src └───────┘ └────┘
typ └───────┘ └────┘
doc └───────┘ └────┘
txt └───────┘ └────┘
par └───────┘ └────┘
pid ┴
st └─────────────────
81 let ⟨N, hN⟩ := pow_unbounded_of_one_lt x⁻¹ hy in
id ┴ └─────────────────────┘ ┴└┘ └┘
src ┴ └┘ └───┘└─────────────────────┘┴ └┘┴ └───
typ ┴ ┴└┘ └───┘└─────────────────────┘┴┴└┘┴└┘└───
doc ┴ └┘ └───┘ ┴ ┴ └───
txt ┴ └┘ └───┘ ┴ ┴ └───
par ┴ └┘ └───┘ ┴ ┴ └───
pid ┴ └┘ └───┘ ┴ ┴ └───
st ─────────────────────────────────────────────────
82 have he: ∃ m : ℤ, y ^ m ≤ x, from
id ┴ ┴ ┴ ┴
src ─┘ └───┘┴└───┘ ┴┴ ┴┴┴ ┴┴┴ └──────
typ ─┘ └───┘┴└───┘ ┴┴ ┴┴┴ ┴┴┴ └──────
doc ─┘ └───┘ └───┘ ┴ ┴ ┴ ┴ ┴ └──────
txt ─┘ └───┘ └───┘ ┴ ┴ ┴ ┴ ┴ └──────
par ─┘ └───┘ └───┘ ┴ ┴ ┴ ┴ ┴ └──────
pid ─┘ └───┘ └───┘ ┴ ┴ ┴ ┴ ┴ └──────
st ────────────────────────────────────
83 ⟨-N, le_of_lt (by rw [(fpow_neg y (↑N)), one_div_eq_inv];
id ┴ └──────┘ └──────┘ ┴ ┴┴ └────────────┘
src ───┘ ┴ └┘└──────┘┴ ┴└──┘ └──────┘┴ ┴ ┴ └──┘└────────────┘┴└─
typ ───┘ ┴ └┘└──────┘┴ ┴└──┘ └──────┘┴┴┴ ┴┴└──┘└────────────┘┴└─
doc ───┘ └┘ ┴ ┴└──┘ ┴ ┴ └──┘ ┴└─
txt ───┘ └┘ ┴ ┴└──┘ ┴ ┴ └──┘ ┴└─
par ───┘ └┘ ┴ ┴└──┘ ┴ ┴ └──┘ ┴└─
pid ───┘ └┘ ┴ └───┘ ┴ ┴ └──┘ └──
st ────────────────────┘└────────────────────┘└──────────────┘┴└─
84 exact (inv_lt hx (lt_trans (inv_pos hx) hN)).1 hN)⟩,
id └────┘ └──────┘ └─────┘ └┘ └┘
src ─────────┘ └────┘┴ ┴ └──────┘┴ └─────┘┴ └┘ └───┘ └──┘
typ ─────────┘ └────┘┴ ┴ └──────┘┴ └─────┘┴└┘└┘ └───┘└┘└──┘
doc ─────────┘ ┴ ┴ ┴ ┴ └┘ └───┘ └──┘
txt ─────────┘ ┴ ┴ ┴ ┴ └┘ └───┘ └──┘
par ─────────┘ ┴ ┴ ┴ ┴ └┘ └───┘ └──┘
pid ─────────┘ ┴ ┴ ┴ ┴ └┘ └───┘ └──┘
st ────────────────────────────────────────────────────┘└───
85 let ⟨M, hM⟩ := pow_unbounded_of_one_lt x hy in
id ┴ └┘
src ┴ └┘ └───┘ ┴ ┴ └───
typ ┴ ┴└┘└┘└───┘ ┴ ┴ └───
doc ┴ └┘ └───┘ ┴ ┴ └───
txt ┴ └┘ └───┘ ┴ ┴ └───
par ┴ └┘ └───┘ ┴ ┴ └───
pid ┴ └┘ └───┘ ┴ ┴ └───
st ───────────────────────────────────────────────
86 have hb: ∃ b : ℤ, ∀ m, y ^ m ≤ x → m ≤ b, from
id ┴
src ─┘ └───┘ └───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────
typ ─┘ └───┘ └───┘ ┴ └┘ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────
doc ─┘ └───┘ └───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────
txt ─┘ └───┘ └───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────
par ─┘ └───┘ └───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────
pid ─┘ └───┘ └───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────
st ─────────────────────────────────────────────────
87 ⟨M, λ m hm, le_of_not_lt (λ hlt, not_lt_of_ge
id └──────────┘ └──────────┘
src ───┘ └┘ └─────┘└──────────┘┴ └────┘└──────────┘└
typ ───┘ └┘ └─────┘└──────────┘┴ └────┘└──────────┘└
doc ───┘ └┘ └─────┘ ┴ └────┘ └
txt ───┘ └┘ └─────┘ ┴ └────┘ └
par ───┘ └┘ └─────┘ ┴ └────┘ └
pid ───┘ └┘ └─────┘ ┴ └────┘ └
st ──────────────────────────────────────────────────
88 (fpow_le_of_le (le_of_lt hy) (le_of_lt hlt)) (lt_of_le_of_lt hm hM))⟩,
id └───────────┘ └────────────┘
src ─┘ └───────────┘┴ ┴ └┘ ┴ └─┘ └────────────┘┴ ┴ └───┘
typ ─┘ └───────────┘┴ ┴ └┘ ┴ └─┘ └────────────┘┴ ┴ └───┘
doc ─┘ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ └───┘
txt ─┘ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ └───┘
par ─┘ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ └───┘
pid ─┘ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ └───┘
st ─────────────────────────────────────────────────────────────────────────
89 let ⟨n, hn₁, hn₂⟩ := int.exists_greatest_of_bdd hb he in
id ┴ └─┘ └─┘ └────────────────────────┘
src ┴ └┘ └┘ └───┘└────────────────────────┘┴ ┴ └───
typ ┴ ┴└┘└─┘└┘└─┘└───┘└────────────────────────┘┴ ┴ └───
doc ┴ └┘ └┘ └───┘ ┴ ┴ └───
txt ┴ └┘ └┘ └───┘ ┴ ┴ └───
par ┴ └┘ └┘ └───┘ ┴ ┴ └───
pid ┴ └┘ └┘ └───┘ ┴ ┴ └───
st ─────────────────────────────────────────────────────────
90 ⟨n, hn₁, lt_of_not_ge (λ hge, not_le_of_gt (int.lt_succ _) (hn₂ _ hge))⟩
id └──────────┘ └──────────┘ └─────────┘
src ─┘ └┘ └┘└──────────┘┴ └────┘└──────────┘┴ └─────────┘└──┘ └─┘ └───
typ ─┘ └┘ └┘└──────────┘┴ └────┘└──────────┘┴ └─────────┘└──┘ └─┘ └───
doc ─┘ └┘ └┘ ┴ └────┘ ┴ └──┘ └─┘ └───
txt ─┘ └┘ └┘ ┴ └────┘ ┴ └──┘ └─┘ └───
par ─┘ └┘ └┘ ┴ └────┘ ┴ └──┘ └─┘ └───
pid ─┘ └┘ └┘ ┴ └────┘ ┴ └──┘ └─┘ └─┘└
st ───────────────────────────────────────────────────────────────────────────
91
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
92 /-- Every positive x is between two successive integer powers of
93 another y greater than one. This is the same as `exists_int_pow_near`,
94 but with ≤ and < the other way around. -/
95 lemma exists_int_pow_near' [discrete_linear_ordered_field α] [archimedean α]
id └───────────────────────────┘ ┴ └─────────┘ ┴
src └───────────────────────────┘ └─────────┘
typ └───────────────────────────┘ ┴ └─────────┘ ┴
96 {x : α} {y : α} (hx : 0 < x) (hy : 1 < y) :
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
97 ∃ n : ℤ, y ^ n < x ∧ x ≤ y ^ (n + 1) :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
98 let ⟨m, hle, hlt⟩ := exists_int_pow_near (inv_pos hx) hy in
id └─┘ ┴ └─────────────────┘ └─────┘ └┘ └┘
src └─────────────────┘ └─────┘
typ └─┘ ┴ └─────────────────┘ └─────┘ └┘ └┘
doc └─────────────────┘
99 have hyp : 0 < y, from lt_trans (discrete_linear_ordered_field.zero_lt_one α) hy,
id ┴ ┴ └──────┘ └───────────────────────────────────────┘ ┴ └┘
src ┴ └──────┘ └───────────────────────────────────────┘
typ ┴ ┴ └──────┘ └───────────────────────────────────────┘ ┴ └┘
100 ⟨-(m+1),
id ┴ ┴
src ┴ ┴
typ ┴ ┴
101 by rwa [fpow_neg, one_div_eq_inv, inv_lt (fpow_pos_of_pos hyp _) hx],
id └──────┘ └────────────┘ └────┘ └─────────────┘ └─┘ └┘
src └───┘└──────┘└┘└────────────┘└┘└────┘┴ └─────────────┘┴ └──┘ ┴
typ └───┘└──────┘└┘└────────────┘└┘└────┘┴ └─────────────┘┴└─┘└──┘└┘┴
doc └───┘ └┘ └┘ ┴ ┴ └──┘ ┴
txt └───┘ └┘ └┘ ┴ ┴ └──┘ ┴
par └───┘ └┘ └┘ ┴ ┴ └──┘ ┴
pid └┘ └┘ └┘ ┴ ┴ └──┘ ┴
st └────────────┘└──────────────┘└─────────────────────────────────┘┴
102 by rwa [neg_add, neg_add_cancel_right, fpow_neg, one_div_eq_inv,
id └─────┘ └──────────────────┘ └──────┘ └────────────┘
src └───┘└─────┘└┘└──────────────────┘└┘└──────┘└┘└────────────┘└─
typ └───┘└─────┘└┘└──────────────────┘└┘└──────┘└┘└────────────┘└─
doc └───┘ └┘ └┘ └┘ └─
txt └───┘ └┘ └┘ └┘ └─
par └───┘ └┘ └┘ └┘ └─
pid └┘ └┘ └┘ └┘ └─
st └───────────┘└────────────────────┘└────────┘└──────────────┘└─
103 le_inv hx (fpow_pos_of_pos hyp _)]⟩
id └────┘ └┘ └─────────────┘ └─┘
src ───────┘└────┘┴ ┴ └─────────────┘┴ └──┘
typ ───────┘└────┘┴└┘┴ └─────────────┘┴└─┘└──┘
doc ───────┘ ┴ ┴ ┴ └──┘
txt ───────┘ ┴ ┴ ┴ └──┘
par ───────┘ ┴ ┴ ┴ └──┘
pid ───────┘ ┴ ┴ ┴ └──┘
st ────────────────────────────────────────┘┴
104
105 variables [linear_ordered_field α] [floor_ring α]
id └──────────────────┘ └────────┘
src └──────────────────┘ └────────┘
typ └──────────────────┘ └────────┘
doc └────────┘
106
107 lemma sub_floor_div_mul_nonneg (x : α) {y : α} (hy : 0 < y) :
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
108 0 ≤ x - ⌊x / y⌋ * y :=
id ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴
doc ┴ ┴
109 begin
st └─────
110 conv in x {rw ← div_mul_cancel x (ne_of_lt hy).symm},
id ┴ └────────────┘ ┴ └──────┘ └┘
src └──────┘ └┘└───┘└────────────┘┴ ┴ └──────┘┴ └────┘┴
typ └──────┘┴└┘└───┘└────────────┘┴┴┴ └──────┘┴└┘└────┘┴
txt └──────┘ └┘└───┘ ┴ ┴ ┴ └────┘┴
par └──────┘ └┘└───┘ ┴ ┴ ┴ └────┘┴
pid ┴└─┘ └─────┘ ┴ ┴ ┴ └─────┘
st ────────────┘└──────────────────────────────────────┘└┘└
111 rw ← sub_mul,
id └─────┘
src └───┘└─────┘
typ └───┘└─────┘
doc └───┘
txt └───┘
par └───┘
pid └─┘
st ─────────────┘└─
112 exact mul_nonneg (sub_nonneg.2 (floor_le _)) (le_of_lt hy)
id └────────┘ └────────┘ └──────┘ └──────┘ └┘
src └────┘└────────┘┴ └────────┘└─┘ └──────┘└───┘ └──────┘┴ └┘
typ └────┘└────────┘┴ └────────┘└─┘ └──────┘└───┘ └──────┘┴└┘└┘
doc └────┘ ┴ └─┘ └───┘ ┴ └┘
txt └────┘ ┴ └─┘ └───┘ ┴ └┘
par └────┘ ┴ └─┘ └───┘ ┴ └┘
pid ┴ ┴ └─┘ └───┘ ┴ ┴┴
st ────────────────────────────────────────────────────────────┘
113 end
st └─┘
114
115 lemma sub_floor_div_mul_lt (x : α) {y : α} (hy : 0 < y) :
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
116 x - ⌊x / y⌋ * y < y :=
id ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc ┴ ┴
117 sub_lt_iff_lt_add.2 begin
id └───────────────┘┴
src └───────────────┘┴
typ └───────────────┘┴
st └─────
118 conv in y {rw ← one_mul y},
id ┴ └─────┘ ┴
src └──────┘ └┘└───┘└─────┘┴ ┴
typ └──────┘┴└┘└───┘└─────┘┴┴┴
txt └──────┘ └┘└───┘ ┴ ┴
par └──────┘ └┘└───┘ ┴ ┴
pid ┴└─┘ └─────┘ ┴ ┴
st ────────────┘└────────────┘└┘└
119 conv in x {rw ← div_mul_cancel x (ne_of_lt hy).symm},
id ┴ └────────────┘ ┴ └──────┘ └┘
src └──────┘ └┘└───┘└────────────┘┴ ┴ └──────┘┴ └────┘┴
typ └──────┘┴└┘└───┘└────────────┘┴┴┴ └──────┘┴└┘└────┘┴
txt └──────┘ └┘└───┘ ┴ ┴ ┴ └────┘┴
par └──────┘ └┘└───┘ ┴ ┴ ┴ └────┘┴
pid ┴└─┘ └─────┘ ┴ ┴ ┴ └─────┘
st ────────────┘└──────────────────────────────────────┘└┘└
120 rw ← add_mul,
id └─────┘
src └───┘└─────┘
typ └───┘└─────┘
doc └───┘
txt └───┘
par └───┘
pid └─┘
st ─────────────┘└─
121 exact (mul_lt_mul_right hy).2 (by rw add_comm; exact lt_floor_add_one _),
id └──────────────┘ └┘ └──────┘ └──────────────┘
src └────┘ └──────────────┘┴ └──┘ ┴└─┘└──────┘└──────┘└──────────────┘└─┘
typ └────┘ └──────────────┘┴└┘└──┘ ┴└─┘└──────┘└──────┘└──────────────┘└─┘
doc └────┘ ┴ └──┘ ┴└─┘ └──────┘ └─┘
txt └────┘ ┴ └──┘ ┴└─┘ └──────┘ └─┘
par └────┘ ┴ └──┘ ┴└─┘ └──────┘ └─┘
pid ┴ ┴ └──┘ └──┘ └──────┘ └─┘
st ──────────────────────────────────┘└────────────────────────────────────┘┴└─
122 end
st ──┘
123
124 end linear_ordered_field
125
126 instance : archimedean ℕ :=
id └─────────┘ ┴
src └─────────┘ ┴
typ └─────────┘ ┴
127 ⟨λ n m m0, ⟨n, by simpa only [mul_one, nat.smul_eq_mul] using nat.mul_le_mul_left n m0⟩⟩
id ┴ ┴ └┘ ┴ └─────┘ └─────────────┘ └─────────────────┘ ┴ └┘
src └──────────┘└─────┘└┘└─────────────┘└──────┘└─────────────────┘┴ ┴
typ ┴ ┴ └┘ ┴ └──────────┘└─────┘└┘└─────────────┘└──────┘└─────────────────┘┴┴┴└┘
doc └──────────┘ └┘ └──────┘ ┴ ┴
txt └──────────┘ └┘ └──────┘ ┴ ┴
par └──────────┘ └┘ └──────┘ ┴ ┴
pid ┴└──┘└┘ └┘ ┴┴└────┘ ┴ ┴
st └───────────────────────────────────────────────────────────────────┘
128
129 instance : archimedean ℤ :=
id └─────────┘ ┴
src └─────────┘ ┴
typ └─────────┘ ┴
130 ⟨λ n m m0, ⟨n.to_nat, le_trans (int.le_to_nat _) $
id ┴ ┴ └┘ ┴└─────┘ └──────┘ └───────────┘
src └─────┘ └──────┘ └───────────┘
typ ┴ ┴ └┘ ┴└─────┘ └──────┘ └───────────┘
131 by simpa only [add_monoid.smul_eq_mul, int.nat_cast_eq_coe_nat, zero_add, mul_one] using mul_le_mul_of_nonneg_left
id └────────────────────┘ └─────────────────────┘ └──────┘ └─────┘ └───────────────────────┘
src └──────────┘└────────────────────┘└┘└─────────────────────┘└┘└──────┘└┘└─────┘└──────┘└───────────────────────┘└
typ └──────────┘└────────────────────┘└┘└─────────────────────┘└┘└──────┘└┘└─────┘└──────┘└───────────────────────┘└
doc └──────────┘ └┘ └┘ └┘ └──────┘ └
txt └──────────┘ └┘ └┘ └┘ └──────┘ └
par └──────────┘ └┘ └┘ └┘ └──────┘ └
pid ┴└──┘└┘ └┘ └┘ └┘ ┴┴└────┘ └
st └────────────────────────────────────────────────────────────────────────────────────────────────────────────────
132 (int.add_one_le_iff.2 m0) (int.coe_zero_le n.to_nat)⟩⟩
id └────────────────┘ └┘ └─────────────┘ └──────┘
src ───┘ └────────────────┘└─┘ └┘ └─────────────┘┴└──────┘┴
typ ───┘ └────────────────┘└─┘└┘└┘ └─────────────┘┴└──────┘┴
doc ───┘ └─┘ └┘ ┴ ┴
txt ───┘ └─┘ └┘ ┴ ┴
par ───┘ └─┘ └┘ ┴ ┴
pid ───┘ └─┘ └┘ ┴ ┴
st ───────────────────────────────────────────────────────┘
133
134 noncomputable def archimedean.floor_ring (α)
135 [linear_ordered_ring α] [archimedean α] : floor_ring α :=
id └─────────────────┘ ┴ └─────────┘ ┴ └────────┘ ┴
src └─────────────────┘ └─────────┘ └────────┘
typ └─────────────────┘ ┴ └─────────┘ ┴ └────────┘ ┴
doc └────────┘
136 { floor := λ x, classical.some (exists_floor x),
id ┴ └────────────┘ └──────────┘ ┴
src └────────────┘ └──────────┘
typ ┴ └────────────┘ └──────────┘ ┴
137 le_floor := λ z x, classical.some_spec (exists_floor x) z }
id ┴ ┴ └─────────────────┘ └──────────┘ ┴ ┴
src └─────────────────┘ └──────────┘
typ ┴ ┴ └─────────────────┘ └──────────┘ ┴ ┴
138
139 section linear_ordered_field
140 variables [linear_ordered_field α]
id └──────────────────┘
src └──────────────────┘
typ └──────────────────┘
141
142 theorem archimedean_iff_nat_lt :
143 archimedean α ↔ ∀ x : α, ∃ n : ℕ, x < n :=
id └─────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src └─────────┘ ┴ ┴ ┴┴ ┴
typ └─────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
144 ⟨@exists_nat_gt α _, λ H, ⟨λ x y y0,
id └───────────┘ ┴ ┴ ┴ ┴ └┘
src └───────────┘
typ └───────────┘ ┴ ┴ ┴ ┴ └┘
145 (H (x / y)).imp $ λ n h, le_of_lt $
id ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └──────┘
src ┴ └─┘ └──────┘
typ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └──────┘
146 by rwa [div_lt_iff y0, ← add_monoid.smul_eq_mul] at h⟩⟩
id └────────┘ └┘ └────────────────────┘
src └───┘└────────┘┴ └──┘└────────────────────┘└────┘
typ └───┘└────────┘┴└┘└──┘└────────────────────┘└────┘
doc └───┘ ┴ └──┘ └────┘
txt └───┘ ┴ └──┘ └────┘
par └───┘ ┴ └──┘ └────┘
pid └┘ ┴ └──┘ ┴└───┘
st └─────────────────┘└────────────────────────┘┴└───┘
147
148 theorem archimedean_iff_nat_le :
149 archimedean α ↔ ∀ x : α, ∃ n : ℕ, x ≤ n :=
id └─────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src └─────────┘ ┴ ┴ ┴┴ ┴
typ └─────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
150 archimedean_iff_nat_lt.trans
id └────────────────────┘└────┘
src └────────────────────┘└────┘
typ └────────────────────┘└────┘
151 ⟨λ H x, (H x).imp $ λ _, le_of_lt,
id ┴ ┴ ┴ ┴ └─┘ ┴ └──────┘
src └─┘ └──────┘
typ ┴ ┴ ┴ ┴ └─┘ ┴ └──────┘
152 λ H x, let ⟨n, h⟩ := H x in ⟨n+1,
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
153 lt_of_le_of_lt h (nat.cast_lt.2 (lt_add_one _))⟩⟩
id └────────────┘ └─────────┘┴ └────────┘
src └────────────┘ └─────────┘┴ └────────┘
typ └────────────┘ └─────────┘┴ └────────┘
154
155 theorem exists_rat_gt [archimedean α] (x : α) : ∃ q : ℚ, x < q :=
id └─────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src └─────────┘ ┴ ┴┴ ┴
typ └─────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
doc ┴
156 let ⟨n, h⟩ := exists_nat_gt x in ⟨n, by rwa rat.cast_coe_nat⟩
id └─┘ ┴ └───────────┘ ┴ └──────────────┘
src └───────────┘ └──┘└──────────────┘
typ └─┘ ┴ └───────────┘ ┴ └──┘└──────────────┘
doc └──┘
txt └──┘
par └──┘
pid ┴
st └───────────────────┘
157
158 theorem archimedean_iff_rat_lt :
159 archimedean α ↔ ∀ x : α, ∃ q : ℚ, x < q :=
id └─────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src └─────────┘ ┴ ┴ ┴┴ ┴
typ └─────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
doc ┴
160 ⟨@exists_rat_gt α _,
id └───────────┘ ┴
src └───────────┘
typ └───────────┘ ┴
161 λ H, archimedean_iff_nat_lt.2 $ λ x,
id ┴ └────────────────────┘┴ ┴
src └────────────────────┘┴
typ ┴ └────────────────────┘┴ ┴
162 let ⟨q, h⟩ := H x in
id └─┘ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴
163 ⟨nat_ceil q, lt_of_lt_of_le h $
id └──────┘ └────────────┘
src └──────┘ └────────────┘
typ └──────┘ └────────────┘
doc └──────┘
164 by simpa only [rat.cast_coe_nat] using (@rat.cast_le α _ _ _).2 (le_nat_ceil _)⟩⟩
id └──────────────┘ └─────────┘ ┴ └─────────┘
src └──────────┘└──────────────┘└──────┘ └─────────┘┴ └────────┘ └─────────┘└─┘
typ └──────────┘└──────────────┘└──────┘ └─────────┘┴┴└────────┘ └─────────┘└─┘
doc └──────────┘ └──────┘ ┴ └────────┘ └─┘
txt └──────────┘ └──────┘ ┴ └────────┘ └─┘
par └──────────┘ └──────┘ ┴ └────────┘ └─┘
pid ┴└──┘└┘ ┴┴└────┘ ┴ └────────┘ └─┘
st └───────────────────────────────────────────────────────────────────────────┘
165
166 theorem archimedean_iff_rat_le :
167 archimedean α ↔ ∀ x : α, ∃ q : ℚ, x ≤ q :=
id └─────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src └─────────┘ ┴ ┴ ┴┴ ┴
typ └─────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
doc ┴
168 archimedean_iff_rat_lt.trans
id └────────────────────┘└────┘
src └────────────────────┘└────┘
typ └────────────────────┘└────┘
169 ⟨λ H x, (H x).imp $ λ _, le_of_lt,
id ┴ ┴ ┴ ┴ └─┘ ┴ └──────┘
src └─┘ └──────┘
typ ┴ ┴ ┴ ┴ └─┘ ┴ └──────┘
170 λ H x, let ⟨n, h⟩ := H x in ⟨n+1,
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
171 lt_of_le_of_lt h (rat.cast_lt.2 (lt_add_one _))⟩⟩
id └────────────┘ └─────────┘┴ └────────┘
src └────────────┘ └─────────┘┴ └────────┘
typ └────────────┘ └─────────┘┴ └────────┘
172
173 variable [archimedean α]
id └─────────┘
src └─────────┘
typ └─────────┘
174
175 theorem exists_rat_lt (x : α) : ∃ q : ℚ, (q : α) < x :=
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc ┴
176 let ⟨n, h⟩ := exists_int_lt x in ⟨n, by rwa rat.cast_coe_int⟩
id └─┘ ┴ └───────────┘ ┴ └──────────────┘
src └───────────┘ └──┘└──────────────┘
typ └─┘ ┴ └───────────┘ ┴ └──┘└──────────────┘
doc └──┘
txt └──┘
par └──┘
pid ┴
st └───────────────────┘
177
178 theorem exists_rat_btwn {x y : α} (h : x < y) : ∃ q : ℚ, x < q ∧ (q:α) < y :=
id ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
179 begin
st └─────
180 cases exists_nat_gt (y - x)⁻¹ with n nh,
id └───────────┘ ┴ ┴ ┴ └┘
src └────┘└───────────┘┴ ┴┴┴ ┴└┘└────────┘
typ └────┘└───────────┘┴ ┴┴┴┴┴┴└┘└────────┘
doc └────┘ ┴ ┴ ┴ ┴ └────────┘
txt └────┘ ┴ ┴ ┴ ┴ └────────┘
par └────┘ ┴ ┴ ┴ ┴ └────────┘
pid ┴ ┴ ┴ ┴ ┴ └────────┘
st ────────────────────────────────────────┘└─
181 cases exists_floor (x * n) with z zh,
id └──────────┘ ┴ ┴ ┴
src └────┘└──────────┘┴ ┴┴┴ └─────────┘
typ └────┘└──────────┘┴ ┴┴┴┴┴└─────────┘
doc └────┘ ┴ ┴ ┴ └─────────┘
txt └────┘ ┴ ┴ ┴ └─────────┘
par └────┘ ┴ ┴ ┴ └─────────┘
pid ┴ ┴ ┴ ┴ ┴└────────┘
st ─────────────────────────────────────┘└─
182 refine ⟨(z + 1 : ℤ) / n, _⟩,
id ┴ ┴ ┴ ┴
src └─────┘ ┴┴└───┘ └┘┴┴ └──┘
typ └─────┘ ┴┴┴└───┘ └┘┴┴┴└──┘
doc └─────┘ ┴ └───┘ └┘ ┴ └──┘
txt └─────┘ ┴ └───┘ └┘ ┴ └──┘
par └─────┘ ┴ └───┘ └┘ ┴ └──┘
pid ┴ ┴ └───┘ └┘ ┴ └──┘
st ────────────────────────────┘└─
183 have n0 := nat.cast_pos.1 (lt_trans (inv_pos (sub_pos.2 h)) nh),
id └──────────┘ └──────┘ └─────┘ └─────┘ ┴ └┘
src └─────────┘└──────────┘└─┘ └──────┘┴ └─────┘┴ └─────┘└─┘ └─┘ ┴
typ └─────────┘└──────────┘└─┘ └──────┘┴ └─────┘┴ └─────┘└─┘┴└─┘└┘┴
doc └─────────┘ └─┘ ┴ ┴ └─┘ └─┘ ┴
txt └─────────┘ └─┘ ┴ ┴ └─┘ └─┘ ┴
par └─────────┘ └─┘ ┴ ┴ └─┘ └─┘ ┴
pid └─────┘┴└─┘ └─┘ ┴ ┴ └─┘ └─┘ ┴
st ────────────────────────────────────────────────────────────────┘└─
184 have n0' := (@nat.cast_pos α _ _).2 n0,
id └──────────┘ ┴ └┘
src └──────────┘ └──────────┘┴ └──────┘
typ └──────────┘ └──────────┘┴┴└──────┘└┘
doc └──────────┘ ┴ └──────┘
txt └──────────┘ ┴ └──────┘
par └──────────┘ ┴ └──────┘
pid └──────┘┴└─┘ ┴ └──────┘
st ───────────────────────────────────────┘└─
185 rw [rat.cast_div_of_ne_zero, rat.cast_coe_nat, rat.cast_coe_int, div_lt_iff n0'],
id └─────────────────────┘ └──────────────┘ └──────────────┘ └────────┘ └─┘
src └──┘└─────────────────────┘└┘└──────────────┘└┘└──────────────┘└┘└────────┘┴ ┴
typ └──┘└─────────────────────┘└┘└──────────────┘└┘└──────────────┘└┘└────────┘┴└─┘┴
doc └──┘ └┘ └┘ └┘ ┴ ┴
txt └──┘ └┘ └┘ └┘ ┴ ┴
par └──┘ └┘ └┘ └┘ ┴ ┴
pid └┘ └┘ └┘ └┘ ┴ ┴
st ────────────────────────────┘└────────────────┘└────────────────┘└──────────────┘└──
186 refine ⟨(lt_div_iff n0').2 $
id └────────┘ └─┘
src └─────┘ └────────┘┴ └──┘ └
typ └─────┘ └────────┘┴└─┘└──┘ └
doc └─────┘ ┴ └──┘ └
txt └─────┘ ┴ └──┘ └
par └─────┘ ┴ └──┘ └
pid ┴ ┴ └──┘ └
st ───────────────────────────────
187 (lt_iff_lt_of_le_iff_le (zh _)).1 (lt_add_one _), _⟩,
id └────────────────────┘ └┘ └────────┘
src ───┘ └────────────────────┘┴ └─────┘ └────────┘└─────┘
typ ───┘ └────────────────────┘┴ └┘└─────┘ └────────┘└─────┘
doc ───┘ ┴ └─────┘ └─────┘
txt ───┘ ┴ └─────┘ └─────┘
par ───┘ ┴ └─────┘ └─────┘
pid ───┘ ┴ └─────┘ └─────┘
st ───────────────────────────────────────────────────────┘└─
188 rw [int.cast_add, int.cast_one],
id └──────────┘ └──────────┘
src └──┘└──────────┘└┘└──────────┘┴
typ └──┘└──────────┘└┘└──────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ─────────────────┘└────────────┘└──
189 refine lt_of_le_of_lt (add_le_add_right ((zh _).1 (le_refl _)) _) _,
id └────────────┘ └──────────────┘ └┘ └─────┘
src └─────┘└────────────┘┴ └──────────────┘┴ └────┘ └─────┘└───────┘
typ └─────┘└────────────┘┴ └──────────────┘┴ └┘└────┘ └─────┘└───────┘
doc └─────┘ ┴ ┴ └────┘ └───────┘
txt └─────┘ ┴ ┴ └────┘ └───────┘
par └─────┘ ┴ ┴ └────┘ └───────┘
pid ┴ ┴ ┴ └────┘ └───────┘
st ────────────────────────────────────────────────────────────────────┘└─
190 rwa [← lt_sub_iff_add_lt', ← sub_mul,
id └────────────────┘ └─────┘
src └─────┘└────────────────┘└──┘└─────┘└─
typ └─────┘└────────────────┘└──┘└─────┘└─
doc └─────┘ └──┘ └─
txt └─────┘ └──┘ └─
par └─────┘ └──┘ └─
pid └──┘ └──┘ └─
st ──────────────────────────┘└─────────┘└─
191 ← div_lt_iff' (sub_pos.2 h), one_div_eq_inv],
id └─────────┘ └─────┘ ┴ └────────────┘
src ────────┘└─────────┘┴ └─────┘└─┘ └─┘└────────────┘┴
typ ────────┘└─────────┘┴ └─────┘└─┘┴└─┘└────────────┘┴
doc ────────┘ ┴ └─┘ └─┘ ┴
txt ────────┘ ┴ └─┘ └─┘ ┴
par ────────┘ ┴ └─┘ └─┘ ┴
pid ────────┘ ┴ └─┘ └─┘ ┴
st ─────────────────────────────────┘└──────────────┘┴└─
192 { rw [rat.coe_int_denom, nat.cast_one], exact one_ne_zero },
id └───────────────┘ └──────────┘ └─────────┘
src └──┘└───────────────┘└┘└──────────┘┴ └────┘└─────────┘┴
typ └──┘└───────────────┘└┘└──────────┘┴ └────┘└─────────┘┴
doc └──┘ └┘ ┴ └────┘ ┴
txt └──┘ └┘ ┴ └────┘ ┴
par └──┘ └┘ ┴ └────┘ ┴
pid └┘ └┘ ┴ ┴ ┴
st ───┘└───────────────────┘└────────────┘└───────────────────┘└┘└
193 { intro H, rw [rat.coe_nat_num, ← coe_coe, nat.cast_eq_zero] at H, subst H, cases n0 },
id └─────────────┘ └─────┘ └──────────────┘ ┴ └┘
src └─────┘ └──┘└─────────────┘└──┘└─────┘└┘└──────────────┘└────┘ └────┘ └────┘ ┴
typ └─────┘ └──┘└─────────────┘└──┘└─────┘└┘└──────────────┘└────┘ └────┘┴ └────┘└┘┴
doc └─────┘ └──┘ └──┘└─────┘└┘ └────┘ └────┘ └────┘ ┴
txt └─────┘ └──┘ └──┘ └┘ └────┘ └────┘ └────┘ ┴
par └─────┘ └──┘ └──┘ └┘ └────┘ └────┘ └────┘ ┴
pid └┘ └┘ └──┘ └┘ ┴└───┘ ┴ ┴ ┴
st ───┘└─────┘└───────────────────┘└─────────┘└────────────────┘┴└───┘└───────┘└─────────┘└┘└
194 { rw [rat.coe_nat_denom, nat.cast_one], exact one_ne_zero }
id └───────────────┘ └──────────┘ └─────────┘
src └──┘└───────────────┘└┘└──────────┘┴ └────┘└─────────┘┴
typ └──┘└───────────────┘└┘└──────────┘┴ └────┘└─────────┘┴
doc └──┘ └┘ ┴ └────┘ ┴
txt └──┘ └┘ ┴ └────┘ ┴
par └──┘ └┘ ┴ └────┘ ┴
pid └┘ └┘ ┴ ┴ ┴
st ────────────────────────┘└────────────┘└───────────────────┘└─
195 end
st ──┘
196
197 theorem exists_nat_one_div_lt {ε : α} (hε : 0 < ε) : ∃ n : ℕ, 1 / (n + 1: α) < ε :=
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
198 begin
st └─────
199 cases archimedean_iff_nat_lt.1 (by apply_instance) (1/ε) with n hn,
id └────────────────────┘ ┴┴
src └────┘└────────────────────┘└─┘ ┴└────────────┘└┘ ┴┴ └─────────┘
typ └────┘└────────────────────┘└─┘ ┴└────────────┘└┘ ┴┴┴└─────────┘
doc └────┘ └─┘ ┴└────────────┘└┘ ┴ └─────────┘
txt └────┘ └─┘ ┴└────────────┘└┘ ┴ └─────────┘
par └────┘ └─┘ ┴└────────────┘└┘ ┴ └─────────┘
pid ┴ └─┘ └───────────────┘ ┴ ┴└────────┘
st ───────────────────────────────────┘└─────────────┘└───────────────┘└─
200 existsi n,
id ┴
src └──────┘
typ └──────┘┴
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
st ──────────┘└─
201 apply div_lt_of_mul_lt_of_pos,
id └─────────────────────┘
src └────┘└─────────────────────┘
typ └────┘└─────────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────────────┘└─
202 { simp, apply add_pos_of_pos_of_nonneg zero_lt_one, apply nat.cast_nonneg },
id └──────────────────────┘ └─────────┘ └─────────────┘
src └──┘ └────┘└──────────────────────┘┴└─────────┘ └────┘└─────────────┘┴
typ └──┘ └────┘└──────────────────────┘┴└─────────┘ └────┘└─────────────┘┴
doc └──┘ └────┘ ┴ └────┘ ┴
txt └──┘ └────┘ ┴ └────┘ ┴
par └──┘ └────┘ ┴ └────┘ ┴
pid ┴ ┴ ┴ ┴
st ───┘└──┘└──────────────────────────────────────────┘└──────────────────────┘└┘└
203 { apply (div_lt_iff' hε).1,
id └─────────┘ └┘
src └────┘ └─────────┘┴ └─┘
typ └────┘ └─────────┘┴└┘└─┘
doc └────┘ ┴ └─┘
txt └────┘ ┴ └─┘
par └────┘ ┴ └─┘
pid ┴ ┴ ┴└┘
st ───────────────────────────┘└─
204 transitivity,
src └──────────┘
typ └──────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
st ───────────────┘└─
205 { exact hn },
id └┘
src └────┘ ┴
typ └────┘└┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────┘└───────┘└┘└
206 { simp [zero_lt_one] }}
id └─────────┘
src └────┘└─────────┘└┘
typ └────┘└─────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ────────────────────────┘└──
207 end
st ──┘
208
209 theorem exists_pos_rat_lt {x : α} (x0 : 0 < x) : ∃ q : ℚ, 0 < q ∧ (q : α) < x :=
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
210 by simpa only [rat.cast_pos] using exists_rat_btwn x0
id └──────────┘ └─────────────┘ └┘
src └──────────┘└──────────┘└──────┘└─────────────┘┴ └
typ └──────────┘└──────────┘└──────┘└─────────────┘┴└┘└
doc └──────────┘ └──────┘ ┴ └
txt └──────────┘ └──────┘ ┴ └
par └──────────┘ └──────┘ ┴ └
pid ┴└──┘└┘ ┴┴└────┘ ┴ └
st └───────────────────────────────────────────────────
211
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
212 include α
213 @[simp] theorem rat.cast_floor (x : ℚ) :
id ┴
src ┴
typ ┴
doc └──┘ ┴
214 by haveI := archimedean.floor_ring α; exact ⌊(x:α)⌋ = ⌊x⌋ :=
id └────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘└────────────────────┘┴ └────┘┴ ┴ ┴┴┴┴┴ ┴
typ └───────┘└────────────────────┘┴┴ └────┘┴ ┴┴┴┴┴┴┴ ┴ ┴
doc └───────┘ ┴ └────┘┴ ┴ ┴┴┴ ┴ ┴
txt └───────┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
par └───────┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
pid ┴└─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st └──────────────────────────────────────────────────────┘
215 begin
st └─────
216 haveI := archimedean.floor_ring α,
id └────────────────────┘ ┴
src └───────┘└────────────────────┘┴
typ └───────┘└────────────────────┘┴┴
doc └───────┘ ┴
txt └───────┘ ┴
par └───────┘ ┴
pid ┴└─┘ ┴
st ──────────────────────────────────┘└─
217 apply le_antisymm,
id └─────────┘
src └────┘└─────────┘
typ └────┘└─────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────┘└─
218 { rw [le_floor, ← @rat.cast_le α, rat.cast_coe_int],
id └──────┘ └─────────┘ ┴ └──────────────┘
src └──┘└──────┘└──┘ └─────────┘┴ └┘└──────────────┘┴
typ └──┘└──────┘└──┘ └─────────┘┴┴└┘└──────────────┘┴
doc └──┘ └──┘ ┴ └┘ ┴
txt └──┘ └──┘ ┴ └┘ ┴
par └──┘ └──┘ ┴ └┘ ┴
pid └┘ └──┘ ┴ └┘ ┴
st ───┘└──────────┘└────────────────┘└────────────────┘└──
219 apply floor_le },
id └──────┘
src └────┘└──────┘┴
typ └────┘└──────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────┘└┘└
220 { rw [le_floor, ← rat.cast_coe_int, rat.cast_le],
id └──────┘ └──────────────┘ └─────────┘
src └──┘└──────┘└──┘└──────────────┘└┘└─────────┘┴
typ └──┘└──────┘└──┘└──────────────┘└┘└─────────┘┴
doc └──┘ └──┘ └┘ ┴
txt └──┘ └──┘ └┘ ┴
par └──┘ └──┘ └┘ ┴
pid └┘ └──┘ └┘ ┴
st ───────────────┘└──────────────────┘└───────────┘└──
221 apply floor_le }
id └──────┘
src └────┘└──────┘┴
typ └────┘└──────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────┘└─
222 end
st ──┘
223
224 end linear_ordered_field
225
226 section
227 variables [discrete_linear_ordered_field α]
id └───────────────────────────┘
src └───────────────────────────┘
typ └───────────────────────────┘
228
229 /-- `round` rounds a number to the nearest integer. `round (1 / 2) = 1` -/
230 def round [floor_ring α] (x : α) : ℤ := ⌊x + 1 / 2⌋
id └────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src └────────┘ ┴ ┴ ┴ ┴ ┴
typ └────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
doc └────────┘ ┴ ┴
231
232 lemma abs_sub_round [floor_ring α] (x : α) : abs (x - round x) ≤ 1 / 2 :=
id └────────┘ ┴ ┴ └─┘ ┴ ┴ └───┘ ┴ ┴ ┴
src └────────┘ └─┘ ┴ └───┘ ┴ ┴
typ └────────┘ ┴ ┴ └─┘ ┴ ┴ └───┘ ┴ ┴ ┴
doc └────────┘ └───┘
233 begin
st └─────
234 rw [round, abs_sub_le_iff],
id └───┘ └────────────┘
src └──┘└───┘└┘└────────────┘┴
typ └──┘└───┘└┘└────────────┘┴
doc └──┘└───┘└┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ──────────┘└──────────────┘└──
235 have := floor_le (x + 1 / 2),
id └──────┘ ┴ ┴ ┴
src └──────┘└──────┘┴ ┴┴└─┘┴└─┘
typ └──────┘└──────┘┴ ┴┴┴└─┘┴└─┘
doc └──────┘ ┴ ┴ └─┘ └─┘
txt └──────┘ ┴ ┴ └─┘ └─┘
par └──────┘ ┴ ┴ └─┘ └─┘
pid └───┘└─┘ ┴ ┴ └─┘ └─┘
st ─────────────────────────────┘└─
236 have := lt_floor_add_one (x + 1 / 2),
id └──────────────┘ ┴
src └──────┘└──────────────┘┴ ┴ └─┘ └─┘
typ └──────┘└──────────────┘┴ ┴┴ └─┘ └─┘
doc └──────┘ ┴ ┴ └─┘ └─┘
txt └──────┘ ┴ ┴ └─┘ └─┘
par └──────┘ ┴ ┴ └─┘ └─┘
pid └───┘└─┘ ┴ ┴ └─┘ └─┘
st ─────────────────────────────────────┘└─
237 split; linarith
src └───┘ └───────┘
typ └───┘ └───────┘
doc └───┘ └───────┘
txt └───┘ └───────┘
par └───┘ └───────┘
pid ┴
st ─────────────────┘
238 end
st └─┘
239
240 variable [archimedean α]
id └─────────┘
src └─────────┘
typ └─────────┘
241
242 theorem exists_rat_near (x : α) {ε : α} (ε0 : 0 < ε) :
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
243 ∃ q : ℚ, abs (x - q) < ε :=
id ┴ ┴┴ └─┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴┴ └─┘ ┴ ┴
typ ┴ ┴┴ └─┘ ┴ ┴ ┴ ┴ ┴
doc ┴
244 let ⟨q, h₁, h₂⟩ := exists_rat_btwn $
id └─┘ ┴ └┘ └┘ └─────────────┘
src └─────────────┘
typ └─┘ ┴ └┘ └┘ └─────────────┘
245 lt_trans ((sub_lt_self_iff x).2 ε0) ((lt_add_iff_pos_left x).2 ε0) in
id └──────┘ └─────────────┘ ┴ ┴ └┘ └─────────────────┘ ┴ ┴ └┘
src └──────┘ └─────────────┘ ┴ └─────────────────┘ ┴
typ └──────┘ └─────────────┘ ┴ ┴ └┘ └─────────────────┘ ┴ ┴ └┘
246 ⟨q, abs_sub_lt_iff.2 ⟨sub_lt.1 h₁, sub_lt_iff_lt_add.2 h₂⟩⟩
id └────────────┘┴ └────┘┴ └───────────────┘┴
src └────────────┘┴ └────┘┴ └───────────────┘┴
typ └────────────┘┴ └────┘┴ └───────────────┘┴
247
248 instance : archimedean ℚ :=
id └─────────┘ ┴
src └─────────┘ ┴
typ └─────────┘ ┴
doc ┴
249 archimedean_iff_rat_le.2 $ λ q, ⟨q, by rw rat.cast_id⟩
id └────────────────────┘┴ ┴ ┴ └─────────┘
src └────────────────────┘┴ └─┘└─────────┘
typ └────────────────────┘┴ ┴ ┴ └─┘└─────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st └─────────────┘
250
251 @[simp] theorem rat.cast_round (x : ℚ) : by haveI := archimedean.floor_ring α;
id ┴ └────────────────────┘ ┴
src ┴ └───────┘└────────────────────┘┴
typ ┴ └───────┘└────────────────────┘┴┴
doc └──┘ ┴ └───────┘ ┴
txt └───────┘ ┴
par └───────┘ ┴
pid ┴└─┘ ┴
st └───────────────────────────────────
252 exact round (x:α) = round x :=
id ┴ ┴ └───┘ ┴
src └────┘ ┴ ┴ └┘┴┴└───┘┴ ┴
typ └────┘ ┴ ┴┴└┘┴┴└───┘┴┴┴
doc └────┘ ┴ ┴ └┘ ┴└───┘┴ ┴
txt └────┘ ┴ ┴ └┘ ┴ ┴ ┴
par └────┘ ┴ ┴ └┘ ┴ ┴ ┴
pid ┴ ┴ ┴ └┘ ┴ ┴ ┴
st ─────────────────────────────┘
253 have ((x + (1 : ℚ) / (2 : ℚ) : ℚ) : α) = x + 1 / 2, by simp,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
doc ┴ ┴ ┴ └──┘
txt └──┘
par └──┘
st └───┘
254 by rw [round, round, ← this, rat.cast_floor]
id └───┘ └───┘ └──┘ └────────────┘
src └──┘└───┘└┘└───┘└──┘ └┘└────────────┘└─
typ └──┘└───┘└┘└───┘└──┘└──┘└┘└────────────┘└─
doc └──┘└───┘└┘└───┘└──┘ └┘ └─
txt └──┘ └┘ └──┘ └┘ └─
par └──┘ └┘ └──┘ └┘ └─
pid └┘ └┘ └──┘ └┘ ┴└
st └────────┘└─────┘└──────┘└──────────────┘┴└
255
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
256 end